package at.ltasat.solve;

import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

import at.ltasat.ArgumentClazzData;
import at.ltasat.CnfFeaturesFactory;
import at.ltasat.CnfClassifierFactories;
import at.ltasat.ArgumentClazzDataClazzManagerIO;
import at.ltasat.classifier.Classification;
import at.ltasat.classifier.Classifier;
import at.ltasat.classifier.io.ClassifierIO;
import at.tasat.cnf.Cnf;
import at.tasat.io.OutputFormatter;
import at.tasat.parser.DimacsParser;

public class SolverMain {

	public static void main(String[] args) {
		SolverConfiguration config = SolverConfiguration.get(args);
		int exit = main(config);
		System.exit(exit);
	}

	public static int main(SolverConfiguration myConfig) {
		final PrintStream out = new PrintStream(myConfig.getOut());
		final PrintStream err = new PrintStream(myConfig.getErr());
		try {
			myConfig.setIn(myConfig.isInFile() ? myConfig.getInFile() : writeToTempFile(myConfig.getIn()));
			if (myConfig.isVerboseConfig()) {
				out.println(OutputFormatter.getCommentString(myConfig.toString()));
			}
			final String[] args = getArgs(myConfig);
			log(myConfig.isVerboseStatus(), out, "running p-tasat with '%s'", new ArrayToString<String>(args));
			at.ptasat.Configuration config = at.ptasat.Configuration.get(args);
			assert myConfig.isInFile();
			config.setIn(myConfig.getInFile());
			config.setOut(out);
			config.setErr(err);
			return at.ptasat.Main.main(config);
		} catch (Throwable error) {
			err.println(OutputFormatter.getErrorString(error));
			return 1;
		}
	}

	private static File writeToTempFile(InputStream in) throws IOException {
		File file = File.createTempFile("l-tasat", ".tmp");
		byte[] buffer = new byte[4096];
		OutputStream out = new FileOutputStream(file);
		for (int nBytes = in.read(buffer); nBytes > 0; nBytes = in.read(buffer)) {
			out.write(buffer, 0, nBytes);
		}
		return file;
	}

	private static String[] getArgs(SolverConfiguration config) throws FileNotFoundException, IOException {
		final List<String> args = new ArrayList<String>();
		for (String arg : config.getArgs()) {
			args.add(arg);
		}
		final Classifier<Cnf, ArgumentClazzData> classifier = ClassifierIO.read(new FileInputStream(config.getClassifierFile()), CnfClassifierFactories.INSTANCE,
				new ArgumentClazzDataClazzManagerIO(), CnfFeaturesFactory.INSTANCE);
		final Cnf cnf = DimacsParser.parse(new FileInputStream(config.getInFile()));
		final Classification<Cnf, ArgumentClazzData> classification = classifier.classify(cnf);
		int nUsedProcessors = 0;
		final List<ArgumentClazzData> more = new ArrayList<ArgumentClazzData>();
		int index = 0;
		while (nUsedProcessors < config.getMax()) {
			ArgumentClazzData data;
			if (index >= classification.getNumberOfMemberships() && more.size() > 0) {
				data = more.get((index - classification.getNumberOfMemberships()) % more.size());
			} else {
				data = classification.getMembership(index++).getClazz().getData();
				if (data.canCreateMore()) {
					more.add(data);
				}
			}
			nUsedProcessors += data.nProcessors();
			args.add(String.format("-w1:%s", data.getArgument()));
		}
		return args.toArray(new String[args.size()]);
	}

	private static void log(boolean verbose, PrintStream out, String msg, Object... args) {
		if (verbose) {
			out.println(OutputFormatter.getCommentString(String.format(msg, args)));
		}
	}

	private static final class ArrayToString<T> {
		private final T[] array;

		public ArrayToString(T[] array) {
			this.array = array;
		}

		@Override
		public String toString() {
			return Arrays.toString(array);
		}
	}
}
